\documentclass{article}
\usepackage{amsfonts}
\usepackage[utf8]{inputenc}
\title{Project Proposal: Verification of Hybrid Systems }
\begin{document}
\maketitle

A hybrid system is a system that has both discrete and continuous behaviour. A good example is a hybrid automaton where the evolution of the system is described by a set of differential equations (continuous behaviour). The automaton can change state (discrete behaviour) and this results in changing the equations that currently describe the evolution of the system. 

Hybrid systems are very complicated and in general the reachability problem for hybrid systems is undecidable. However, there are subclasses of hybrid systems for which reachability is actually decidable, for instance some subclasses of linear hybrid systems.
\\

A possible direction for a PhD research project would be to try and push the frontier of hybrid systems for which reachability is decidable. I would begin by analysing the existing results and methods and then try to look for improvements and new methods in the area. A good place to start would be to follow in the footsteps of Lafferriere et al. and their paper "A New Class of Decidable Hybrid Systems"\cite{Lafferriere:1999:NCD:646879.710437}. In this paper they show that linear hybrid systems that admit certain regularity properties have decidable reachability problems. 
\\

Another direction would be to study the possibility of making an abstraction over a hybrid system that would allow for analysis of its properties. The abstraction could for instance be a timed automaton. If the original hybrid system is a set of linear differential equations each representing a state of the system, e.g. temperature as a function of time, we could define the timed automaton to have the same set of states as the hybrid system, but the timed automaton would record only the timed behaviour of the hybrid system. States of the timed automaton then correspond to certain intervals of temperature. Maybe an abstraction of this type could be used to analyse the properties of general hybrid systems.

Upon finding an appropriate abstraction of a hybrid system and finding out how to use it to calculate properties of the original hybrid system, the natural step would be to implement this functionality in a tool. 
\\

I suggest to be supervised by Kim Guldstrand Larsen with a possible co-supervision by someone from the Department of Mathematics at Aalborg University.

\bibliographystyle{plain}
\bibliography{bib}
\end{document}
